… and EvalDist/BitVec

Both files contained lemmas generic over any `m` with `[HasEvalSPMF m]` but
incorrectly imported from OracleComp, violating the EvalDist → OracleComp
layering. List.lean needed no split — just import and namespace fixes.
BitVec.lean's SampleableType instance moved to SampleableType.lean.
README updated to fix outdated notation (++ₒ→+, [=x|]→Pr[=x|], etc.).

Made-with: Cursor

… bound

Extend Fork.lean with seed-slot collision probability bounds and the global collision penalty lemma, then wire these into le_probOutput_fork while leaving the final seed-factor/square step explicitly marked for continuation.

Made-with: Cursor

Add agent guidance to keep unfinished Lean proof structure with local `stop` checkpoints instead of deleting blocks, so later iterations can continue from prior search context.

Made-with: Cursor

Adopt independence as the canonical perfect-secrecy definition with equivalent formulations, so privacy statements align with textbook semantics and are easier to reuse. Prove one-time-pad privacy against the new notion and document the updated proof status.

Add reusable perfect-secrecy experiment decomposition lemmas and complete the backward Shannon direction constructively. Make the forward direction explicit via a passed hypothesis so the theorem family is fully sorry-free while keeping proof obligations transparent.

Replace the misleading Shannon iff path with an explicit constructive theorem over `perfectSecrecyAt`, and add the stronger PMF-prior theorem that proves uniform+unique implies all-priors secrecy. This keeps theorem semantics honest while preserving reusable proof helpers.

- Extract ENNReal Cauchy-Schwarz inequalities to ToMathlib/Data/ENNReal/SumSquares.lean
- Factor out cipherGivenMsg_uniform_of_uniformKey_of_uniqueKey in SymmEncAlg.lean,
  derive both Shannon theorems and ciphertextRowsEqualAt from it
- Remove unused perfectSecrecyAt_iff_allDefs / perfectSecrecy_iff_allDefs lemmas
- Move XOR probability lemmas to OracleComp/Constructions/BitVec.lean
- Add generic probEvent_liftComp_uniformSample_eq_of_eq helper in SeededOracle.lean,
  simplify seed-slot collision lemmas in Fork.lean
- Extract length_eq_of_mem_support_generateSeed to deduplicate repeated blocks

Net -150 lines.

Made-with: Cursor

Delete ~390 lines of old forking lemma code that used obsolete API
(guard, getM, [= x | ...] notation, s+1 index bug). All theorem
statements are now covered by the active uncommented code.

Made-with: Cursor

Made-with: Cursor